not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
↳ QTRS
↳ DependencyPairsProof
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
AND2(x, or2(y, z)) -> AND2(x, z)
NOT1(or2(x, y)) -> AND2(not1(x), not1(y))
AND2(x, or2(y, z)) -> AND2(x, y)
AND2(or2(y, z), x) -> AND2(x, z)
AND2(or2(y, z), x) -> AND2(x, y)
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
AND2(x, or2(y, z)) -> AND2(x, z)
NOT1(or2(x, y)) -> AND2(not1(x), not1(y))
AND2(x, or2(y, z)) -> AND2(x, y)
AND2(or2(y, z), x) -> AND2(x, z)
AND2(or2(y, z), x) -> AND2(x, y)
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
AND2(x, or2(y, z)) -> AND2(x, z)
AND2(x, or2(y, z)) -> AND2(x, y)
AND2(or2(y, z), x) -> AND2(x, z)
AND2(or2(y, z), x) -> AND2(x, y)
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND2(x, or2(y, z)) -> AND2(x, z)
AND2(x, or2(y, z)) -> AND2(x, y)
AND2(or2(y, z), x) -> AND2(x, z)
AND2(or2(y, z), x) -> AND2(x, y)
POL(AND2(x1, x2)) = x1 + 2·x2
POL(or2(x1, x2)) = 1 + 2·x1 + 2·x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(y)
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT1(and2(x, y)) -> NOT1(x)
NOT1(and2(x, y)) -> NOT1(y)
Used ordering: Polynomial interpretation [21]:
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
POL(NOT1(x1)) = x1
POL(and2(x1, x2)) = 1 + 2·x1 + x2
POL(or2(x1, x2)) = x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT1(or2(x, y)) -> NOT1(x)
NOT1(or2(x, y)) -> NOT1(y)
POL(NOT1(x1)) = 2·x1
POL(or2(x1, x2)) = 1 + 2·x1 + x2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
not1(not1(x)) -> x
not1(or2(x, y)) -> and2(not1(x), not1(y))
not1(and2(x, y)) -> or2(not1(x), not1(y))
and2(x, or2(y, z)) -> or2(and2(x, y), and2(x, z))
and2(or2(y, z), x) -> or2(and2(x, y), and2(x, z))